The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

fibs_2#1(zipwith_l, plus, tail_l, x3) → ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0) → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(x7, cond_take_l_n_xs(fibs_2#1(x4, x8, x12, bot[0]), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(x7, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12, bot[0]), x16))
plus#2(0, x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3, bot[6]), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[6]), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5, x3) → cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2, x1) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5, bot[7]), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2, x1) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5, bot[7]), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), x12)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

fibs_2#1(zipwith_l, plus, tail_l, x3) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(x7, cond_take_l_n_xs(fibs_2#1(x4, x8, x12, bot[0]), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(x7, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12, bot[0]), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3, bot[6]), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[6]), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5, x3) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2, x1) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5, bot[7]), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2, x1) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5, bot[7]), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
fibs_2#1/3
Cons/0
zipwith_l_f_xs_ys#1/3

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
cond_take_l_n_xs, zipwith_l_f_xs_ys#1, plus#2, cond_zipwith_l_f_xs_ys

They will be analysed ascendingly in the following order:
zipwith_l_f_xs_ys#1 < cond_take_l_n_xs
zipwith_l_f_xs_ys#1 = cond_zipwith_l_f_xs_ys

(8) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

The following defined symbols remain to be analysed:
plus#2, cond_take_l_n_xs, zipwith_l_f_xs_ys#1, cond_zipwith_l_f_xs_ys

They will be analysed ascendingly in the following order:
zipwith_l_f_xs_ys#1 < cond_take_l_n_xs
zipwith_l_f_xs_ys#1 = cond_zipwith_l_f_xs_ys

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

Induction Base:
plus#2(gen_0':S8_0(0), gen_0':S8_0(b)) →_R^Ω(1)
gen_0':S8_0(b)

Induction Step:
plus#2(gen_0':S8_0(+(n12_0, 1)), gen_0':S8_0(b)) →_R^Ω(1)
S(plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b))) →_IH
S(gen_0':S8_0(+(b, c13_0)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

The following defined symbols remain to be analysed:
cond_zipwith_l_f_xs_ys, cond_take_l_n_xs, zipwith_l_f_xs_ys#1

They will be analysed ascendingly in the following order:
zipwith_l_f_xs_ys#1 < cond_take_l_n_xs
zipwith_l_f_xs_ys#1 = cond_zipwith_l_f_xs_ys

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol cond_zipwith_l_f_xs_ys.

(13) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

The following defined symbols remain to be analysed:
zipwith_l_f_xs_ys#1, cond_take_l_n_xs

They will be analysed ascendingly in the following order:
zipwith_l_f_xs_ys#1 < cond_take_l_n_xs
zipwith_l_f_xs_ys#1 = cond_zipwith_l_f_xs_ys

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)) → *11_0, rt ∈ Ω(n7664₀)

Induction Base:
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0))

Induction Step:
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(n7664_0, 1))) →_R^Ω(1)
cond_zipwith_l_f_xs_ys(fibs_2#1(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(n7664_0, 1))) →_R^Ω(1)
cond_zipwith_l_f_xs_ys(ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l))), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(1, n7664_0))) →_R^Ω(1)
cond_zipwith_l_f_xs_ys(ConsL(S(0'), zipwith_l_f_xs_ys(plus, fibs, fibs_2(zipwith_l, plus, tail_l))), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(1, n7664_0))) →_R^Ω(1)
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)), S(0'), zipwith_l_f_xs_ys(plus, fibs, fibs_2(zipwith_l, plus, tail_l))) →_IH
cond_zipwith_l_f_xs_ys_1(*11_0, S(0'), zipwith_l_f_xs_ys(plus, fibs, fibs_2(zipwith_l, plus, tail_l)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)) → *11_0, rt ∈ Ω(n7664₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

The following defined symbols remain to be analysed:
cond_zipwith_l_f_xs_ys, cond_take_l_n_xs

They will be analysed ascendingly in the following order:
zipwith_l_f_xs_ys#1 < cond_take_l_n_xs
zipwith_l_f_xs_ys#1 = cond_zipwith_l_f_xs_ys

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol cond_zipwith_l_f_xs_ys.

(18) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)) → *11_0, rt ∈ Ω(n7664₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

The following defined symbols remain to be analysed:
cond_take_l_n_xs

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol cond_take_l_n_xs.

(20) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)) → *11_0, rt ∈ Ω(n7664₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

No more defined symbols left to analyse.

(21) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

(22) BOUNDS(n^1, INF)

(23) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)
zipwith_l_f_xs_ys#1(plus, gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(n7664_0)) → *11_0, rt ∈ Ω(n7664₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

(25) BOUNDS(n^1, INF)

(26) Obligation:

Innermost TRS:
Rules:
fibs_2#1(zipwith_l, plus, tail_l) → ConsL(S(0'), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
cond_take_l_n_xs(ConsL(x16, x18), 0') → Nil
cond_take_l_n_xs(ConsL(x7, fibs_2(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(fibs_2#1(x4, x8, x12), x16))
cond_take_l_n_xs(ConsL(x7, zipwith_l_f_xs_ys(x4, x8, x12)), S(x16)) → Cons(cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4, x8, x12), x16))
plus#2(0', x12) → x12
plus#2(S(x4), x2) → S(plus#2(x4, x2))
cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) → ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3))
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), zipwith_l_f_xs_ys(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1, x2, x3), x5, x4)
cond_zipwith_l_f_xs_ys(ConsL(x5, x4), fibs_2(x1, x2, x3)) → cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3), x5, x4)
zipwith_l_f_xs_ys#1(plus, fibs, x5) → cond_zipwith_l_f_xs_ys(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x5)
zipwith_l_f_xs_ys#1(plus, fibs_2(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(fibs_2#1(x3, x4, x5), x2)
zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(x3, x4, x5), x2) → cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3, x4, x5), x2)
zipwith_l#3(x8, x4) → zipwith_l_f_xs_ys(plus, x8, x4)
main(x12) → cond_take_l_n_xs(ConsL(0', fibs_2(zipwith_l, plus, tail_l)), x12)

Types:
fibs_2#1 :: zipwith_l → plus → tail_l → ConsL
zipwith_l :: zipwith_l
plus :: plus
tail_l :: tail_l
ConsL :: 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
S :: 0':S → 0':S
0' :: 0':S
zipwith_l#3 :: fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
fibs :: fibs:fibs_2:zipwith_l_f_xs_ys
fibs_2 :: zipwith_l → plus → tail_l → fibs:fibs_2:zipwith_l_f_xs_ys
cond_take_l_n_xs :: ConsL → 0':S → Nil:Cons
Nil :: Nil:Cons
Cons :: Nil:Cons → Nil:Cons
zipwith_l_f_xs_ys :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys
zipwith_l_f_xs_ys#1 :: plus → fibs:fibs_2:zipwith_l_f_xs_ys → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
plus#2 :: 0':S → 0':S → 0':S
cond_zipwith_l_f_xs_ys_1 :: ConsL → 0':S → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
cond_zipwith_l_f_xs_ys :: ConsL → fibs:fibs_2:zipwith_l_f_xs_ys → ConsL
main :: 0':S → Nil:Cons
hole_ConsL1_0 :: ConsL
hole_zipwith_l2_0 :: zipwith_l
hole_plus3_0 :: plus
hole_tail_l4_0 :: tail_l
hole_0':S5_0 :: 0':S
hole_fibs:fibs_2:zipwith_l_f_xs_ys6_0 :: fibs:fibs_2:zipwith_l_f_xs_ys
hole_Nil:Cons7_0 :: Nil:Cons
gen_0':S8_0 :: Nat → 0':S
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0 :: Nat → fibs:fibs_2:zipwith_l_f_xs_ys
gen_Nil:Cons10_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_0':S8_0(0) ⇔ 0'
gen_0':S8_0(+(x, 1)) ⇔ S(gen_0':S8_0(x))
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(0) ⇔ fibs_2(zipwith_l, plus, tail_l)
gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(+(x, 1)) ⇔ zipwith_l_f_xs_ys(plus, fibs_2(zipwith_l, plus, tail_l), gen_fibs:fibs_2:zipwith_l_f_xs_ys9_0(x))
gen_Nil:Cons10_0(0) ⇔ Nil
gen_Nil:Cons10_0(+(x, 1)) ⇔ Cons(gen_Nil:Cons10_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
plus#2(gen_0':S8_0(n12_0), gen_0':S8_0(b)) → gen_0':S8_0(+(n12_0, b)), rt ∈ Ω(1 + n12₀)

(28) BOUNDS(n^1, INF)